Nuprl Lemma : es-interface-image_wf
11,40
postcript
pdf
es
:ES,
A
,
B
:Type,
f
:(
A
B
),
Ia
:AbsInterface(
A
).
f
'
Ia
AbsInterface(
B
)
latex
Definitions
Top
,
t
T
,
left
+
right
,
x
:
A
.
B
(
x
)
,
E
,
x
:
A
B
(
x
)
,
f
(
a
)
,
inl
x
,
x
.
A
(
x
)
,
f
o
g
,
Type
,
ES
,
f
'
Ia
,
AbsInterface(
A
)
Lemmas
p-compose
wf
,
es-E
wf
,
top
wf
origin
es:ES, A, B:Type, f:(A
B), Ia:AbsInterface(A). f'Ia 
AbsInterface(B) es:ES, A, B:Type, f:(AB), Ia:AbsInterface(A). f'Ia AbsInterface(B) Tx:A. B(x)B(x)
x.A(x)